(set-logic QF_AUFBV)
(declare-sort OutOfBoundsValueIs_s 0)
(declare-fun reset_f (OutOfBoundsValueIs_s) Bool)
(declare-fun readAddr_f (OutOfBoundsValueIs_s) (_ BitVec 2))
(declare-fun m_out_MPORT_rand_data_f (OutOfBoundsValueIs_s) (_ BitVec 8))
(declare-fun m_f (OutOfBoundsValueIs_s) (Array (_ BitVec 2) (_ BitVec 8)))
(declare-fun _resetCount_f (OutOfBoundsValueIs_s) Bool)
(define-fun m.out_MPORT.addr_f ((state OutOfBoundsValueIs_s)) (_ BitVec 2) (readAddr_f state))
(define-fun m.out_MPORT.data_f ((state OutOfBoundsValueIs_s)) (_ BitVec 8) (select (m_f state) (m.out_MPORT.addr_f state)))
(define-fun m_out_MPORT_addr_f ((state OutOfBoundsValueIs_s)) (_ BitVec 2) (readAddr_f state))
(define-fun m_out_MPORT_oob_f ((state OutOfBoundsValueIs_s)) Bool (not (bvugt (_ bv3 2) (m_out_MPORT_addr_f state))))
(define-fun m_out_MPORT_rand_data.en_f ((state OutOfBoundsValueIs_s)) Bool (m_out_MPORT_oob_f state))
(define-fun _T_f ((state OutOfBoundsValueIs_s)) Bool (= (readAddr_f state) (_ bv0 2)))
(define-fun out_f ((state OutOfBoundsValueIs_s)) (_ BitVec 8) (ite (m_out_MPORT_oob_f state) (m_out_MPORT_rand_data_f state) (m.out_MPORT.data_f state)))
(define-fun _T_1_f ((state OutOfBoundsValueIs_s)) Bool (= (out_f state) (_ bv0 8)))
(define-fun _T_3_f ((state OutOfBoundsValueIs_s)) Bool (not (reset_f state)))
(define-fun _T_4_f ((state OutOfBoundsValueIs_s)) Bool (not (_T_1_f state)))
(define-fun _T_5_f ((state OutOfBoundsValueIs_s)) Bool (= (readAddr_f state) (_ bv1 2)))
(define-fun _T_10_f ((state OutOfBoundsValueIs_s)) Bool (= (readAddr_f state) (_ bv2 2)))
(define-fun _T_15_f ((state OutOfBoundsValueIs_s)) Bool (= (readAddr_f state) (_ bv3 2)))
(define-fun _resetPhase_f ((state OutOfBoundsValueIs_s)) Bool (not (bvuge (ite (_resetCount_f state) (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun assert_f ((state OutOfBoundsValueIs_s)) Bool (=> (and (_T_f state) (_T_3_f state)) (_T_1_f state)))
(define-fun assert_1_f ((state OutOfBoundsValueIs_s)) Bool (=> (and (_T_5_f state) (_T_3_f state)) (_T_1_f state)))
(define-fun assert_2_f ((state OutOfBoundsValueIs_s)) Bool (=> (and (_T_10_f state) (_T_3_f state)) (_T_1_f state)))
(define-fun assert_3_f ((state OutOfBoundsValueIs_s)) Bool (=> (and (_T_15_f state) (_T_3_f state)) (_T_1_f state)))
(define-fun _resetActive_f ((state OutOfBoundsValueIs_s)) Bool (=> (_resetPhase_f state) (reset_f state)))
(define-fun m.out_MPORT.en_f ((state OutOfBoundsValueIs_s)) Bool true)
(define-fun m_next ((state OutOfBoundsValueIs_s)) (Array (_ BitVec 2) (_ BitVec 8)) (m_f state))
(define-fun const_array_0 ((index (_ BitVec 2))) (_ BitVec 8) (_ bv0 8))
(define-fun m_init ((state OutOfBoundsValueIs_s)) (Array (_ BitVec 2) (_ BitVec 8)) const_array_0)
(define-fun _resetCount_next ((state OutOfBoundsValueIs_s)) Bool (ite (_resetPhase_f state) (= ((_ extract 0 0) (bvadd ((_ zero_extend 1) (ite (_resetCount_f state) (_ bv1 1) (_ bv0 1))) (_ bv1 2))) (_ bv1 1)) (_resetCount_f state)))
(define-fun _resetCount_init ((state OutOfBoundsValueIs_s)) Bool false)
(define-fun OutOfBoundsValueIs_t ((state OutOfBoundsValueIs_s) (state_n OutOfBoundsValueIs_s)) Bool (and (= (m_f state_n) (m_next state)) (= (_resetCount_f state_n) (_resetCount_next state))))
(define-fun OutOfBoundsValueIs_i ((state OutOfBoundsValueIs_s)) Bool (and (= (m_f state) (m_init state)) (= (_resetCount_f state) (_resetCount_init state))))
(define-fun OutOfBoundsValueIs_a ((state OutOfBoundsValueIs_s)) Bool (and (assert_f state) (and (assert_1_f state) (and (assert_2_f state) (assert_3_f state)))))
(define-fun OutOfBoundsValueIs_u ((state OutOfBoundsValueIs_s)) Bool (_resetActive_f state))
(declare-fun s0 () OutOfBoundsValueIs_s)
(assert (OutOfBoundsValueIs_i s0))
(assert (_resetActive_f s0))
(assert (not (and (assert_f s0) (and (assert_1_f s0) (and (assert_2_f s0) (assert_3_f s0))))))
(check-sat)
